feat: prototype update action #5
Conversation
| Run `lake update` and then investigate why this update causes the lean build to fail. | ||
| Files changed in update: ${{ steps.check-update.outputs.changed_files }} | ||
|
|
||
| # To do: Update action so that it will not create another issue until this present issue is closed. |
There was a problem hiding this comment.
If tracking issues is tricky, this is a good compromise since we can easily close the old one by hand
There was a problem hiding this comment.
A previous version had a bit of code which detected if there was still an issue produced from a prior run and then avoid creating a new issue. However it didn't work as expected and I failed to find my error. I'm sure it was just something stupid with the syntax. Another day I'll be able to find a way.
However I'm uncertain exactly what behaviour is preferred when it detects that an update is available but needs manual intervention. Options are:
- Open new issue only if there is no open issue from a prior run
- Close the prior issue and open a new issue
- Do nothing with issues and send a message to the maintainers
- Fail the workflow so notify the maintainers that there is something to do
We'll see what is best as we progress. I return to focus on completing the stuff in topology. It's been going well and soon should be done. Sebastien suggested to me to PR the alternate version of Cantor's theorem which we use into mathlib so that's also in progress.
Talk to you on Thursday!
There was a problem hiding this comment.
I think "Fail the workflow so notify the maintainers that there is something to do" is already enough, at least I would see it in my github notifications anyway.
"Open new issue only if there is no open issue from a prior run" is a stronger signal than just a job failure, since in this case I would also get an email. I don't mind if it does not close the job though
|
I just noticed that the action failed. In the repo's Settings -> Actions -> General there is an option to allow actions to open pull requests. This needs to be activated for the new action to work properly. |
|
Done! |
Now our action can do some work for us! |
There didn't appear to be any actions available for doing this task.
This workflow will periodically run
lean updateand trylean buildif there is an available update.There are three possible outcomes:
I've tested it quite a bit and seems to do as required. Are you will for us to try it for a while?
I would like to improve some of the details once I clearly understand what is most comfortable and then package it as an easy to use action for others.